Example 3.3.25 in [Borralleras - PhD'03]

Summary: Ex3_3_25_Bor03

• CS-TRS format
• OBJ format
• Negative results:
• Positive results:
  1. Lucas' transformation (Polynomials @ MuTerm)
  2. Giesl and Middeldorp's transformation (Metacombination @ AProVE)
  3. CSRPO
  4. Polynomials (MuTerm)
  5. CSDP

CS-TRS Ex3_3_25_Bor03 (file Ex3_3_25_Bor03.csr)

Functions:  app nil cons from s zWadr prefix

Constructors:  nil cons s

Variables:  YS X XS Y L

Arities: 

ar(app) = 2
ar(nil) = 0
ar(cons) = 2
ar(from) = 1
ar(s) = 1
ar(zWadr) = 2
ar(prefix) = 1

Replacement map: 

&181;(app)={1,2}
&181;(nil)={}
&181;(cons)={1}
&181;(from)={1}
&181;(s)={1}
&181;(zWadr)={1,2}
&181;(prefix)={1}

Rules: (file Ex3_3_25_Bor03)  

app(nil,YS) -> YS
app(cons(X,XS),YS) -> cons(X,app(XS,YS))
from(X) -> cons(X,from(s(X)))
zWadr(nil,YS) -> nil
zWadr(XS,nil) -> nil
zWadr(cons(X,XS),cons(Y,YS)) -> cons(app(Y,cons(X,nil)),zWadr(XS,YS))
prefix(L) -> cons(nil,zWadr(L,prefix(L)))

The CS-TRS in OBJ format (file Ex3_3_25_Bor03.obj):

obj Ex3_3_25_Bor03 is
  sort S .
  op app : S S -> S .
  op nil : -> S .
  op cons : S S -> S [strat (1 0)] .
  op from : S -> S .
  op s : S -> S .
  op zWadr : S S -> S .
  op prefix : S -> S .
  vars YS X XS Y L : S .
  eq app(nil,YS) = YS .
  eq app(cons(X,XS),YS) = cons(X,app(XS,YS)) .
  eq from(X) = cons(X,from(s(X))) .
  eq zWadr(nil,YS) = nil .
  eq zWadr(XS,nil) = nil .
  eq zWadr(cons(X,XS),cons(Y,YS)) = cons(app(Y,cons(X,nil)),zWadr(XS,YS)) .
  eq prefix(L) = cons(nil,zWadr(L,prefix(L))) .
endo

Negative results

Positive results

1. Ex3_3_25_Bor03 can be proved µ-terminating by using Lucas' transformation. The TRS Ex3_3_25_Bor03_L:

   app(nil,YS) -> YS
   app(cons(X),YS) -> cons(X)
   from(X) -> cons(X)
   zWadr(nil,YS) -> nil
   zWadr(XS,nil) -> nil
   zWadr(cons(X),cons(Y)) -> cons(app(Y,cons(X)))
   prefix(L) -> cons(nil)
   

   is terminating (use MuTerm).
2. The µ-termination of Ex3_3_25_Bor03 can be proved by using Giesl and Middeldorp's transformation: The TRS Ex3_3_25_Bor03_GM:

   a__app(nil,YS) -> mark(YS)
   a__app(cons(X,XS),YS) -> cons(mark(X),app(XS,YS))
   a__from(X) -> cons(mark(X),from(s(X)))
   a__zWadr(nil,YS) -> nil
   a__zWadr(XS,nil) -> nil
   a__zWadr(cons(X,XS),cons(Y,YS)) -> cons(a__app(mark(Y),cons(mark(X),nil)),zWadr(XS,YS))
   a__prefix(L) -> cons(nil,zWadr(L,prefix(L)))
   mark(app(X1,X2)) -> a__app(mark(X1),mark(X2))
   mark(from(X)) -> a__from(mark(X))
   mark(zWadr(X1,X2)) -> a__zWadr(mark(X1),mark(X2))
   mark(prefix(X)) -> a__prefix(mark(X))
   mark(nil) -> nil
   mark(cons(X1,X2)) -> cons(mark(X1),X2)
   mark(s(X)) -> s(mark(X))
   a__app(X1,X2) -> app(X1,X2)
   a__from(X) -> from(X)
   a__zWadr(X1,X2) -> zWadr(X1,X2)
   a__prefix(X) -> prefix(X)
   

   is terminating (use Metacombination with AProVE).
3. The µ-termination of Ex3_3_25_Bor03 is proved in [Bor03, Example 3.3.25] by using CSRPO and automatically by MuTerm:
   • marking map:

            m(cons,2)=m(_cons,2)=m(_app,1)=m(_zWadr,1)={from,app,zWadr}
            m(zWadr,2)={from,app,zWadr,prefix}
            

   • precedence:

            zWadr = _zWadr > cons,app,nil
            app = _app > cons
            from > cons,_from,s
            prefix > cons,nil,_zWadr,_prefix
            

   • status:

            st(f)=mul for all symbols f.
            

4. The µ-termination of Ex3_3_25_Bor03 can also be proved by using a polynomial interpretation (computed with MuTerm):

   Proof of termination for CS-TRS  Ex3_3_25_Bor03:
   
   [app](X1,X2) = X1 + X2 + 1
   [nil] = 0
   [cons](X1,X2) = X1
   [from](X) = X + 1
   [s](X) = X
   [zWadr](X1,X2) = X1 + X2 + 2
   [prefix](X) = X + 1
   

5. The µ-termination of Ex3_3_25_Bor03 can also be proved by using CSDP (computed by MuTerm).